Nuprl Lemma : nil_member-variant
11,40
postcript
pdf
T
,
A
:Type,
x
:
T
. (
A
r
T
)
((
x
[])
False)
latex
ProofTree
Definitions
t
T
,
P
Q
,
False
,
A
,
A
B
,
,
{
x
:
A
|
B
(
x
)}
,
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
Void
,
x
:
A
B
(
x
)
,
A
c
B
,
x
:
A
.
B
(
x
)
,
#$n
,
||
as
||
,
a
<
b
,
type
List
,
[]
,
l
[
i
]
,
s
=
t
,
Type
,
,
P
Q
,
P
&
Q
,
P
Q
,
(
x
l
)
Lemmas
nat
wf
,
length
wf2
,
select
wf
,
false
wf
origin
T, A:Type, x:T. (A 
r T) 
((x 
[]) 
False)
T, A:Type, x:T. (A r T) ((x []) False)
T Q
A
B
B(x)x:A. B(x)
B(x)
B
x:A. B(x)
Q Q l)